minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
↳ QTRS
↳ DependencyPairsProof
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
DIV(s(X), s(Y)) → DIV(minus(X, Y), s(Y))
DIV(s(X), s(Y)) → IF(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
MINUS(s(X), s(Y)) → MINUS(X, Y)
GEQ(s(X), s(Y)) → GEQ(X, Y)
DIV(s(X), s(Y)) → MINUS(X, Y)
DIV(s(X), s(Y)) → GEQ(X, Y)
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
DIV(s(X), s(Y)) → DIV(minus(X, Y), s(Y))
DIV(s(X), s(Y)) → IF(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
MINUS(s(X), s(Y)) → MINUS(X, Y)
GEQ(s(X), s(Y)) → GEQ(X, Y)
DIV(s(X), s(Y)) → MINUS(X, Y)
DIV(s(X), s(Y)) → GEQ(X, Y)
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
GEQ(s(X), s(Y)) → GEQ(X, Y)
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GEQ(s(X), s(Y)) → GEQ(X, Y)
The value of delta used in the strict ordering is 15/8.
POL(s(x1)) = 1/2 + (13/4)x_1
POL(GEQ(x1, x2)) = (15/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
MINUS(s(X), s(Y)) → MINUS(X, Y)
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MINUS(s(X), s(Y)) → MINUS(X, Y)
The value of delta used in the strict ordering is 15/8.
POL(MINUS(x1, x2)) = (15/4)x_2
POL(s(x1)) = 1/2 + (13/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
DIV(s(X), s(Y)) → DIV(minus(X, Y), s(Y))
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIV(s(X), s(Y)) → DIV(minus(X, Y), s(Y))
The value of delta used in the strict ordering is 1.
POL(minus(x1, x2)) = 0
POL(DIV(x1, x2)) = (4)x_1
POL(s(x1)) = 1/4 + (1/4)x_1
POL(0) = 0
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y